Kripke–Platek set theory
Kripke–Platek set theory is a first-order axiomatic set theory that is weaker than Zermelo–Fraenkel set theory.http://cantorsattic.info/Kripke-Platek It uses the language of set theory, with infinitely many set variables, denoted by letters, and two set connectives \(=\), \(\in\). Axioms Under the name there are several axiomatic systems - a system without axiom of infinity (abbreviated KP or KP-), one with axiom of infinity (abbreviated KPω or KPI, but some authors use KP), one with axiom schema of \(\in\)-induction (some authors use KP) instead of axiom of foundation, one with axiom of \(\Pi_1\)-foundation instead of axiom of foundation (some authors use KP), and so on. Therefore one needs to be very careful when he or she refers to proof-theoretic statements on Kripke-Platek set theory without sources. Unfortunately, several "well-known" results on proof theory of Kripke-Platek set theory are unpublished, and hence many articles available on the internet lack sufficient sources. Axiom of Extensionality \x\forall y(\forall z(z\in x\leftrightarrow z\in y)\rightarrow x=y)\ Given sets \(x\), \(y\), if they have exactly the same elements, then they are equal. Axiom of Empty Set \x\forall y(y\notin x)\ where \(y\notin x\) is shorthand for \(\neg y\in x\). There exists some set. In fact, there is a set which contains no members. Axiom of Pairing \x\forall y\exists z\forall w(w\in z\leftrightarrow(w=x\lor w=y))\ Given sets \(x\), \(y\), there exists a set \(z=\{x,y\}\). Axiom of Union \x\exists y\forall z(z\in y\leftrightarrow\exists w(z\in w\land w\in x))\ For every set \(x\), there exists a set \(y\) whose members are exactly all the members of the members of \(x\), denoted \(y=\bigcup x\) or \(y=\bigcup_{z\in x}z\). Axiom Schema of Foundation For every formula \(\phi(x,p_1,\cdots,p_n)\) or abbreviated \(\phi(x,\vec{p})\), the following is an instance of the axiom schema: \x\phi(x,\vec{p})\rightarrow\exists x(\phi(x,\vec{p})\land\neg\exists y(y\in x\land\phi(y,\vec{p}))))\ Suppose that a given property \(\phi\) is true for some set \(x\). Then there is a \(\in\)-minimal set for which \(\phi\) is true. Some authors restrict the axiom shema to \(\Pi_1\)-formulae. On the other hand, some authors call the axiom schema of \(\in\)-induction "axiom schema of foundation". Axiom Schema of \(\Sigma_0\)-Separation A \(\Sigma_0\) formula is a formula in which every occurrence of quantifier is bounded, namely in the form \(\forall x\in y\phi\) (i.e. \(\forall x(x\in y\rightarrow\phi)\)) or \(\exists x\in y\phi\) (i.e. \(\exists x(x\in y\land\phi)\)). (See for \(\Sigma_n\), \(\Pi_n\) and \(\Delta_n\) formulas) For every \(\Sigma_0\) formula \(\phi(x,\vec{p})\), the following is an instance of the axiom schema: \x\exists y\forall z(z\in y\leftrightarrow(z\in x\land\phi(z,\vec{p})))\ Given a set \(x\), there exists a set \(y=\{z\in x|\phi(z,\vec{p})\}\). Axiom Schema of \(\Sigma_0\)-Collection For every \(\Sigma_0\) formula \(\phi(x,y,\vec{p})\), the following is an instance of the axiom schema: \a(\forall x\in a\exists y\phi(x,y,\vec{p})\rightarrow\exists b\forall x\in a\exists y\in b\phi(x,y,\vec{p}))\ Given a set \(a\), if for all its member \(x\) there is some \(y\) such that \((x,y)\) satisfies a given \(\Sigma_0\)-property, then there exists a set \(b\) such that such \(y\) can be found in \(b\). Axiom of Infinity \x(\varnothing\in x\land\forall y\in x(y\cup\{y\}\in x))\ where \(\varnothing\in x\) is shorthand for \(\exists y\in x\forall z(\neg z\in y)\), and \(y\cup\{y\}\in x\) is shorthand for \(\exists z\in x\forall w(w\in z\leftrightarrow(w\in y\lor w=y))\). There exists a set containing infinitely many elements, and it follows from this axiom that the empty set exists. Some authors use other formulations such as the following: \x(\exists z(z\in x) \land(\forall y\in x\exists z\in x(y\in z)))\ There exists a set containing a finite \(\in\)-chain of elements of any length, and it does not follow from this axiom that the empty set exists. Axiom Schema of \(\in\)-induction For every formula \(\phi(x)\), the following is an instance of the axiom schema: \x(\forall y\in x\phi(y)\rightarrow\phi(x))\rightarrow\forall x\phi(x)\ Suppose that a given property \(\phi\) is true for any set \(x\) such that \(\phi\) is true for any \(y\in x\). Then \(\phi\) is true for any set \(x\). Open-induction, which is the axiom schema of \(\in\)-induction restricted to open formulae, follows from other axiomsDomenico Zambella, "Foundation versus Induction in Kripke-Platek Set Theory", The Journal of Symbolic Logic, Vol. 63, No. 4 (Dec., 1998), pp. 1399-1403.. Subsystems Subsystems of KPω are derived by restricted axiom schema of foundation. Foundation on \(\Pi_n\) formulas (respectively, \(\Sigma_n\) formulas) \(\phi\) is denoted \(\Pi_n\)-Foundation (respectively, \(\Sigma_n\)-Foundation). The weakest system, denoted KPω'''0, is '''KPω without foundation. The proof-theoretic ordinal (abbreviated PTO) of KPω is the Bachmann-Howard ordinal, while those subsystems have smaller PTO. The PTO of \(\text{KP}\omega^0+\Sigma_1\text{-Foundation}\) is \(\varphi(\varphi(\omega,0),0)\). For \(n\ge2\), the PTO of \(\text{KP}\omega^0+\Pi_n\text{-Foundation}\) is \(\psi_\Omega(\delta_n)\) where \(\delta_0=\omega\) and \(\delta_{i+1}=\Omega^{\delta_i}\).Michael Rathjen, "Fragments of Kripke–Platek Set Theory with Infinity" Axiom of Regularity The full foundation implies axiom of regularity. Adding Regularity to KPω'0 results a stronger system, denoted '''KPω'r. Induction on Natural Numbers The full foundation also implies the induction schema of natural numbers (denoted IND). For every \(\Sigma_n\) formula \(\phi(x)\), the following is an instance of the \(\Sigma_n\)-induction schema (denoted \(\Sigma_n\)-IND): \x\in\omega(\phi(x)\rightarrow\phi(x+1)))\rightarrow\forall x\in\omega\phi(x)\ where \(\omega\) is the first limit ordinal. IND is then the conjunction of \(\Sigma_n\)-IND for all n. With restricted foundation, IND improves PTO of the system. \(\text{KP}\omega^0+\Pi_1\text{-Foundation}+\Sigma_1\text{-IND}\) has a PTO of \(\varphi(\omega^\omega,0)\), \(\text{KP}\omega^0+\Pi_1\text{-Foundation}+\text{IND}\) has a PTO of \(\varphi(\varepsilon_0,0)\), and \(\text{KP}\omega^0+\Sigma_1\text{-Foundation}+\text{IND}\) has a PTO of \(\varphi(\varphi(\varepsilon_0,0),0)\). For \(n\ge2\), the PTO of \(\text{KP}\omega^0+\Pi_n\text{-Foundation}+\text{IND}\) is \(\psi_\Omega(\delta_n)\) where \(\delta_0=\varepsilon_0\) and \(\delta_{i+1}=\Omega^{\delta_i}\). Extensions Compared with '''ZFC, KPω lacks axiom of power set and axiom of choice; separation and collection are also restricted on \(\Sigma_0\) formulas. So adding these axioms to KPω is an extension. Axiom Schema of Separation Let \(\Sigma_n\)-Sep (respectively, \(\Delta_n\)-Sep) denote the axiom schema of separation working on \(\Sigma_n\) formulas (respectively, \(\Delta_n\) formulas). \(\text{KP}\omega^r+\text{IND}+\Sigma_1\text{-Sep}\) and \(\Pi^1_2\text{-CA}\) prove the same sentences of second-order arithmetic; \(\text{KP}\omega+\Sigma_1\text{-Sep}\) and \(\Pi^1_2\text{-CA}+\text{BI}\) also prove the same sentences of second-order arithmetic.Michael Rathjen, "Explicit Mathematics With The Monotone Fixed Point Principle. II: Models" Let \(L\) denote the constructible hierarchy. The least ordinal \(\beta\) satisfying \(L_\beta\models\text{KP}\omega+\Sigma_1\text{-Sep}\) and \(L_\beta\cap\mathcal P(\omega)\models\Pi^1_2\text{-CA}+\text{BI}\) are equal; the least \(\beta\) for \(L_\beta\models\text{KP}\omega+\Delta_2\text{-Sep}\) and \(L_\beta\cap\mathcal P(\omega)\models\Delta^1_3\text{-CA}\) are equal; the least \(\beta\) for \(L_\beta\models\text{KP}\omega+\text{Sep}\), \(L_\beta\models\)ZFC without axiom of power set, and \(L_\beta\cap\mathcal P(\omega)\models \text{Z}_2\) are also equal.David A. Madore, "A zoo of ordinals" Axiom Schema of Collection Let \(\Sigma_n\)-Coll denote the axiom schema of collection working on \(\Sigma_n\) formulas. For \(n>0\), \(\text{KP}\omega+\Sigma_n\text{-Sep}+\Sigma_n\text{-Coll}\) and \(\Pi^1_{n+1}\text{-CA}+\Sigma^1_{n+1}\text{-AC}+\text{BI}\) prove the same sentences of second-order arithmetic.Michael Rathjen, "The Higher Infinite in Proof Theory" Axiom of Power Set KPω with axiom of power set (denoted Pow) is strong enough to dwarf the strength of second-order arithmetic, but it can't prove the existence of \(V_{\omega2}\).Michael Rathjen, "Relativized ordinal analysis: The case of Power Kripke-Platek set theory" Power Kripke–Platek set theory, denoted \(\text{KP}(\mathcal P)\), is \(\text{KP}\omega+\text{Pow}+\Delta^{\mathcal P}_0\text{-Sep}+\Delta^{\mathcal P}_0\text{-Coll}\), where \(\Delta^{\mathcal P}_0\)-Sep (respectively, \(\Delta^{\mathcal P}_0\)-Coll) is the axiom schema of separation (respectively, axiom schema of collection) only applied on \(\Delta^{\mathcal P}_0\) formulas. A \(\Delta^{\mathcal P}_0\) formula is a formula in which every occurrence of quantifier is in the form \(\forall x\in y\phi\), \(\exists x\in y\phi\), \(\forall x\subseteq y\phi\) (i.e. \(\forall x(\forall z(z\in x\rightarrow z\in y)\rightarrow\phi)\)) or \(\exists x\subseteq y\phi\) (i.e. \(\exists x(\forall z(z\in x\rightarrow z\in y)\land\phi)\)). \(\text{KP}(\mathcal P)\) enable separation and collection on \(\Delta^{\mathcal P}_0\) properties, and it is much stronger than KPω + Pow. The least ordinal \(\alpha\) for "\(V_\alpha\) is a \(\Pi^{\mathcal P}_2\) model of \(\text{KP}(\mathcal P)\)" is the Bachmann-Howard ordinal. Axiom of Choice \(\text{KP}(\mathcal P)\) with axiom of choice (denoted AC), however, still have equal PTO to \(\text{KP}(\mathcal P)\).Michael Rathjen, "Power Kripke-Platek set theory and the axiom of choice" Large Ordinal Axioms Large ordinal axioms on KP usually use definitions in model theory. The first large ordinals are usually countable, and KP with these axioms is weaker than KPω + Pow. Admissible Ordinals A set \(A\) is admissible if it is a transitive model of KP, denoted \(A\models\text{KP}\). Ordinal \(\alpha\) is called an admissible ordinal if \(L_\alpha\) is an admissible set. Some authors use another formulation of the admissibility characterised by the following axioms: # If \(A\) is admissible, then \(A\) is a transitive model of the axioms of pair, union, \(\Delta_0\)-separation, \(\Delta_0\)-collection, and infinity. # If \(A\) and \(B\) are admissible, then either one of \(A \in B\), \(A = B\), or \(B \in A\) holds. The least admissible ordinal is \(\omega\), followed by \(\omega^\text{CK}_1\). The ordinal \(\omega^\text{CK}_{\alpha+1}\) is defined to be next admissible after \(\omega^\text{CK}_\alpha\), and \(\omega^\text{CK}_\alpha=\sup\{\omega^\text{CK}_\beta|\beta<\alpha\}\) for a limit ordinal \(\alpha\). \(\omega^\text{CK}_\omega\), the first limit of admissible ordinals, is not admissible. KPl is KP asserting "the universe is a limit of admissible sets", with a PTO of Takeuti-Feferman-Buchholz ordinal.https://ncatlab.org/nlab/show/ordinal+analysis For some authors, KPI means KPω. Recursively Inaccessible and Mahlo Ordinals An ordinal is recursively inaccessible if it is admissible and is a limit of admissible ordinals. Analogously, a set \(x\) is recursively inaccessible if it is admissible and \(\forall y\in x\exists z\in x(y\in z\land\,z\text{ is admissible})\). KPi is KP asserting "the universe is recursively inaccessible", with a PTO of \(\psi_\Omega(\varepsilon_{I+1})\), in an ordinal notation using a weakly inaccessible cardinal \(I\). And \(L_\alpha\models\text{KPi}\) iff ordinal \(\alpha\) is recursively inaccessible. The lack of Foundation results a much weaker system, KPi'''0, with a PTO of Feferman–Schütte ordinal. Higher recursive inaccessibility can be defined similarly: an ordinal is recursively \(\alpha\)-inaccessible if it is admissible and is a limit of recursively \(\beta\)-inaccessible ordinals for all \(\beta<\alpha\). An ordinal \(\alpha\) is recursively hyperinaccessible if it is \(\alpha\)-inaccessible. A set \(x\) is recursively Mahlo if it is admissible, and for every \(\Sigma_0\) formula \(\phi(y,z,\vec{p})\), \(\forall\vec{p}\in x(\forall y\in x\exists z\in x\phi(y,z,\vec{p})\rightarrow\exists w\in x(w\text{ is admissible}\land\vec{p}\in w\land\forall y\in w\exists z\in w\phi(y,z,\vec{p})))\). Ordinal \(\alpha\) is called a recursively Mahlo ordinal if \(L_\alpha\) is a recursively Mahlo set.Anton Setzer, "Universes in Type Theory Part I – Inaccessibles and Mahlo" A recursively Mahlo is recursively inaccessible, recursively 2-inaccessible, recursively hyperinaccessible, and a limit of such ordinals. '''KPM is KP asserting "the universe is recursively Mahlo". Since it is not convenient to formulate KPM in the way above for the purpose of ordinal analysis, some authors use another formulation given by derivation system with cut-elimination. It has PTO \(\psi_\Omega(\varepsilon_{M+1})\) (in an ordinal collapsing function using a weakly Mahlo cardinal \(M\)), while the system without Foundation, KPM'''0, has PTO \(\varphi(\omega,0,0)\). The proof of the claim on PTO of '''KPM seems unpublished, but at least, a deeply related comparison to \(\psi_\Omega(\psi_{\chi_{\varepsilon_{M+1}}(0)}(0))\) is published.Michael Rathjen, Collapsing functions based on recursively large ordinals: A well–ordering proof for KPM. Archive for Mathematical Logic 33 (1994) 35–55. Reflecting Ordinals An ordinal \(\alpha\) is \(\Pi_n^m\)-reflecting (respectively, \(\Sigma_n^m\)-reflecting) if for every \(m+1\)-th order \(\Pi_n\) sentence (respectively, \(\Sigma_n\) sentence) \(\phi\), \L_\alpha\models\phi\rightarrow\exists\beta<\alpha(L_\beta\models\phi)\ \(\Pi_n^0\)-reflecting (respectively, \(\Sigma_n^0\)-reflecting) is also written as \(\Pi_n\)-reflecting (respectively, \(\Sigma_n\)-reflecting). An ordinal \(\alpha\) is \(\Pi_n^m\)-reflecting on class \(X\) if for every \(m+1\)-th order \(\Pi_n\) sentence \(\phi\), \X\cap\alpha(L_\beta\models\phi)\ \(\Pi_1\)-reflecting ordinals are weak: \(\alpha\) is \(\Pi_1\)-reflecting on \(X\) iff \(\alpha=\sup(X\cap\alpha)\). An ordinal is \(\Pi_2\)-reflecting iff it is admissible\(>\omega\). An ordinal is recursively Mahlo iff it is \(\Pi_2\)-reflecting on admissible ordinals.Wayne Richter and Peter Aczel, "Inductive Definitions and Reflecting Properties of Admissible Ordinals" An ordinal is \(\Pi_n\)-reflecting iff it is \(\Sigma_{n+1}\)-reflecting. \(\text{KP}+\Pi_n\text{-Ref}\) is KP with the axiom schema for all \(\Pi_n\) formulas \(\phi(\vec{p})\): \(\forall\vec{p}(\phi(\vec{p})\rightarrow\exists x(x\models\phi(\vec{p})))\). \(\text{KP}+\Pi_3\text{-Ref}\) has PTO \(\psi_\Omega(\varepsilon_{K+1})\), in an ordinal notation using a weakly compact cardinal \(K\). And \(L_\alpha\models\text{KP}+\Pi_n\text{-Ref}\) iff \(\alpha\) is \(\Pi_n\)-reflecting. \(\text{KP}+\Pi_\omega\text{-Ref}\) is KP with the axiom schema for all first-order formulas \(\phi(\vec{p})\): \(\forall\vec{p}(\phi(\vec{p})\rightarrow\exists x(x\models\phi(\vec{p})))\). It has PTO \(\Psi_{\mathbb X}^{\varepsilon_{\Xi+1}}\) where \(\mathbb X=(\omega^+;\text{P}_0;\epsilon;\epsilon;0)\), in an ordinal notation using a \(\Pi_0^2\)-indescribable cardinal \(\Xi\).Jan-Carl Stegert, "Ordinal proof theory of Kripke-Platek set theory augmented by strong reflection principles" And \(L_\alpha\models\text{KP}+\Pi_\omega\text{-Ref}\) iff \(\alpha\) is \(\Pi_0^1\)-reflecting. Stable ordinals Stable ordinals are defined using \(\Sigma_n\)-elementary substructure on levels of . Class M is a \(\Sigma_n\)-elementary substructure of N if it is a substructure of N and for every \(\Sigma_n\) formula \(\phi(\vec{p})\), \(M\models\phi(\vec{p})\leftrightarrow N\models\phi(\vec{p})\), denoted \(M\prec_{\Sigma_n}N\). For \(n\ge1\), a countable ordinal \(\alpha\) is \(n\)-stable if \(L_\alpha\prec_{\Sigma_n}L\); for \(\rho>\alpha\), a countable ordinal \(\alpha\) is \((\rho,n)\)-stable if \(L_\alpha\prec_{\Sigma_n}L_\rho\). There are special definitions for \(\Sigma_1\)-elementary substructures:http://cantorsattic.info/Stable *A countable ordinal \(\alpha\) is \((+\beta)\)-stable if \(L_\alpha\prec_{\Sigma_1}L_{\alpha+\beta}\). *A countable ordinal \(\alpha\) is \((^+)\)-stable if \(L_\alpha\prec_{\Sigma_1}L_\beta\) where \(\beta\) is next admissible ordinal after \(\alpha\). *A countable ordinal \(\alpha\) is \((^{++})\)-stable if \(L_\alpha\prec_{\Sigma_1}L_\beta\) where \(\beta\) is next admissible ordinal after the admissible ordinal after \(\alpha\). *A countable ordinal \(\alpha\) is inaccessibly-stable if \(L_\alpha\prec_{\Sigma_1}L_\beta\) where \(\beta\) is next recursively inaccessible ordinal after \(\alpha\). *A countable ordinal \(\alpha\) is Mahlo-stable if \(L_\alpha\prec_{\Sigma_1}L_\beta\) where \(\beta\) is next recursively Mahlo ordinal after \(\alpha\). *A countable ordinal \(\alpha\) is doubly \((+\beta)\)-stable if there exists ordinal \(\gamma\) such that \(L_\alpha\prec_{\Sigma_1}L_\gamma\prec_{\Sigma_1}L_{\gamma+\beta}\). *A countable ordinal \(\alpha\) is nonprojectable if \(\sup\{\beta<\alpha|L_\beta\prec_{\Sigma_1}L_\alpha\}=\alpha\). *A countable ordinal \(\alpha\) is stable if \(L_\alpha\prec_{\Sigma_1}L\). \((\rho,1)\)-stability has the following properties:Jon Barwise, "Admissible Sets and Structures", page 179 #If \(\alpha<\beta<\gamma\) and \(L_\alpha\prec_{\Sigma_1}L_\gamma\), then \(L_\alpha\prec_{\Sigma_1}L_\beta\). #If \(L_\alpha\prec_{\Sigma_1}L_\beta\) and \(L_\beta\prec_{\Sigma_1}L_\gamma\), then \(L_\alpha\prec_{\Sigma_1}L_\gamma\). #If \(\alpha<\beta\) and \(\beta\) is stable, then \(\alpha\) is stable iff \(L_\alpha\prec_{\Sigma_1}L_\beta\). #If a set \(A\) is nonempty and \(\forall\alpha\in A(L_\alpha\prec_{\Sigma_1}L_\beta)\), then \(L_{\sup A}\prec_{\Sigma_1}L_\beta\). (+1)-stable ordinals are exactly \(\Pi_0^1\)-reflecting ordinals. \((^+)\)-stable ordinals are exactly \(\Pi_1^1\)-reflecting ordinals. The least \(\Sigma_1^1\)-reflecting ordinal is greater than the least \(\Pi_1^1\)-reflecting ordinal, but every \((^{++})\)-stable ordinal is \(\Sigma_1^1\)-reflecting. Stable ordinals are exactly \(\Sigma_2^1\)-reflecting ordinals, while the least of them is less than the least \(\Pi_2^1\)-reflecting ordinal.Wayne Richter, "The Least \(\Sigma^1_2\) and \(\Pi^1_2\) Reflecting Ordinals", ISILC Logic Conference, ISBN 3-540-07534-8, 568–578 \(\zeta\), the supremum of all eventually writable ordinals, is the least ordinal \(\alpha\) that is \((\rho,2)\)-stable for some \(\rho\); and \(\Sigma\), the supremum of all accidentally writable ordinals, is the least ordinal \(\rho\) such that \(\zeta\) is \((\rho,2)\)-stable. Ansten Mørch Klev, "Extending Kleene’s O Using Inﬁnite Time Turing Machines" For a countable ordinal \(\alpha\), \(\alpha\) is nonprojectable iff \(L_\alpha\models\text{KP}\omega+\Sigma_1\text{-Sep}\). For a limit ordinal \(\alpha\), \(L_\alpha\models\Sigma_n\text{-Sep}+\Sigma_n\text{-Coll}\) iff \(\forall x\in L_\alpha\exists M\in L_\alpha(x\subseteq M\land M\prec_{\Sigma_n}L_\alpha)\). The set theory Stability is KPi with the axiom \(\forall\alpha\exists\beta(\alpha\le\beta\land L_\beta\prec_{\Sigma_1}L_{\beta+\alpha})\). It has PTO \(\Psi_{\mathbb X}^{\varepsilon_{\Upsilon+1}}\) where \(\mathbb X=(\omega^+;\text{P}_0;\epsilon;\epsilon;0)\), in an ordinal notation using such \(\Upsilon\) that \(\forall\alpha<\Upsilon\exists\kappa<\Upsilon(\kappa\text{ is }\alpha\text{-indescribable})\land\forall\alpha<\Upsilon\forall\kappa<\Upsilon(\kappa\text{ is }\alpha\text{-indescribable}\rightarrow\alpha<\kappa)\). Sources See also ja:KP集合論 Category:Set theory